Termination w.r.t. Q proof of /tmp/aprove_benchmark_example

Termination w.r.t. Q of the following Term Rewriting System could not be shown:

Q restricted rewrite system:
The TRS R consists of the following rules:

app(app(app(rec, f), x), 0) → x
app(app(app(rec, f), x), app(s, y)) → app(app(f, app(s, y)), app(app(app(rec, f), x), y))

Q is empty.

↳ QTRS

  ↳ Overlay + Local Confluence

Q restricted rewrite system:
The TRS R consists of the following rules:

app(app(app(rec, f), x), 0) → x
app(app(app(rec, f), x), app(s, y)) → app(app(f, app(s, y)), app(app(app(rec, f), x), y))

Q is empty.

The TRS is overlay and locally confluent. By [19] we can switch to innermost.

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

app(app(app(rec, f), x), 0) → x
app(app(app(rec, f), x), app(s, y)) → app(app(f, app(s, y)), app(app(app(rec, f), x), y))

The set Q consists of the following terms:

app(app(app(rec, x0), x1), 0)
app(app(app(rec, x0), x1), app(s, x2))

Using Dependency Pairs [1,15] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

APP(app(app(rec, f), x), app(s, y)) → APP(f, app(s, y))
APP(app(app(rec, f), x), app(s, y)) → APP(app(app(rec, f), x), y)
APP(app(app(rec, f), x), app(s, y)) → APP(app(f, app(s, y)), app(app(app(rec, f), x), y))

The TRS R consists of the following rules:

app(app(app(rec, f), x), 0) → x
app(app(app(rec, f), x), app(s, y)) → app(app(f, app(s, y)), app(app(app(rec, f), x), y))

The set Q consists of the following terms:

app(app(app(rec, x0), x1), 0)
app(app(app(rec, x0), x1), app(s, x2))

We have to consider all minimal (P,Q,R)-chains.

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ Narrowing

          ↳ MNOCProof

Q DP problem:
The TRS P consists of the following rules:

APP(app(app(rec, f), x), app(s, y)) → APP(f, app(s, y))
APP(app(app(rec, f), x), app(s, y)) → APP(app(app(rec, f), x), y)
APP(app(app(rec, f), x), app(s, y)) → APP(app(f, app(s, y)), app(app(app(rec, f), x), y))

The TRS R consists of the following rules:

app(app(app(rec, f), x), 0) → x
app(app(app(rec, f), x), app(s, y)) → app(app(f, app(s, y)), app(app(app(rec, f), x), y))

The set Q consists of the following terms:

app(app(app(rec, x0), x1), 0)
app(app(app(rec, x0), x1), app(s, x2))

We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule APP(app(app(rec, f), x), app(s, y)) → APP(app(f, app(s, y)), app(app(app(rec, f), x), y)) at position [1] we obtained the following new rules:

APP(app(app(rec, x0), x1), app(s, 0)) → APP(app(x0, app(s, 0)), x1)
APP(app(app(rec, x0), x1), app(s, app(s, x2))) → APP(app(x0, app(s, app(s, x2))), app(app(x0, app(s, x2)), app(app(app(rec, x0), x1), x2)))

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ Narrowing

            ↳ QDP

              ↳ ForwardInstantiation

          ↳ MNOCProof

Q DP problem:
The TRS P consists of the following rules:

APP(app(app(rec, x0), x1), app(s, 0)) → APP(app(x0, app(s, 0)), x1)
APP(app(app(rec, x0), x1), app(s, app(s, x2))) → APP(app(x0, app(s, app(s, x2))), app(app(x0, app(s, x2)), app(app(app(rec, x0), x1), x2)))
APP(app(app(rec, f), x), app(s, y)) → APP(f, app(s, y))
APP(app(app(rec, f), x), app(s, y)) → APP(app(app(rec, f), x), y)

The TRS R consists of the following rules:

app(app(app(rec, f), x), 0) → x
app(app(app(rec, f), x), app(s, y)) → app(app(f, app(s, y)), app(app(app(rec, f), x), y))

The set Q consists of the following terms:

app(app(app(rec, x0), x1), 0)
app(app(app(rec, x0), x1), app(s, x2))

We have to consider all minimal (P,Q,R)-chains.
By forward instantiating [14] the rule APP(app(app(rec, f), x), app(s, y)) → APP(f, app(s, y)) we obtained the following new rules:

APP(app(app(rec, app(app(rec, y_0), y_1)), x1), app(s, x2)) → APP(app(app(rec, y_0), y_1), app(s, x2))
APP(app(app(rec, app(app(rec, y_0), y_1)), x1), app(s, 0)) → APP(app(app(rec, y_0), y_1), app(s, 0))
APP(app(app(rec, app(app(rec, y_0), y_1)), x1), app(s, app(s, y_2))) → APP(app(app(rec, y_0), y_1), app(s, app(s, y_2)))

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ Narrowing

            ↳ QDP

              ↳ ForwardInstantiation

                ↳ QDP

                  ↳ ForwardInstantiation

          ↳ MNOCProof

Q DP problem:
The TRS P consists of the following rules:

APP(app(app(rec, x0), x1), app(s, 0)) → APP(app(x0, app(s, 0)), x1)
APP(app(app(rec, x0), x1), app(s, app(s, x2))) → APP(app(x0, app(s, app(s, x2))), app(app(x0, app(s, x2)), app(app(app(rec, x0), x1), x2)))
APP(app(app(rec, app(app(rec, y_0), y_1)), x1), app(s, x2)) → APP(app(app(rec, y_0), y_1), app(s, x2))
APP(app(app(rec, app(app(rec, y_0), y_1)), x1), app(s, 0)) → APP(app(app(rec, y_0), y_1), app(s, 0))
APP(app(app(rec, f), x), app(s, y)) → APP(app(app(rec, f), x), y)
APP(app(app(rec, app(app(rec, y_0), y_1)), x1), app(s, app(s, y_2))) → APP(app(app(rec, y_0), y_1), app(s, app(s, y_2)))

The TRS R consists of the following rules:

app(app(app(rec, f), x), 0) → x
app(app(app(rec, f), x), app(s, y)) → app(app(f, app(s, y)), app(app(app(rec, f), x), y))

The set Q consists of the following terms:

app(app(app(rec, x0), x1), 0)
app(app(app(rec, x0), x1), app(s, x2))

We have to consider all minimal (P,Q,R)-chains.
By forward instantiating [14] the rule APP(app(app(rec, f), x), app(s, y)) → APP(app(app(rec, f), x), y) we obtained the following new rules:

APP(app(app(rec, x0), x1), app(s, app(s, app(s, y_2)))) → APP(app(app(rec, x0), x1), app(s, app(s, y_2)))
APP(app(app(rec, x0), x1), app(s, app(s, y_2))) → APP(app(app(rec, x0), x1), app(s, y_2))
APP(app(app(rec, app(app(rec, y_0), y_1)), x1), app(s, app(s, 0))) → APP(app(app(rec, app(app(rec, y_0), y_1)), x1), app(s, 0))
APP(app(app(rec, x0), x1), app(s, app(s, 0))) → APP(app(app(rec, x0), x1), app(s, 0))
APP(app(app(rec, app(app(rec, y_0), y_1)), x1), app(s, app(s, y_3))) → APP(app(app(rec, app(app(rec, y_0), y_1)), x1), app(s, y_3))
APP(app(app(rec, app(app(rec, y_0), y_1)), x1), app(s, app(s, app(s, y_3)))) → APP(app(app(rec, app(app(rec, y_0), y_1)), x1), app(s, app(s, y_3)))

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ Narrowing

            ↳ QDP

              ↳ ForwardInstantiation

                ↳ QDP

                  ↳ ForwardInstantiation

                    ↳ QDP

                      ↳ MNOCProof

          ↳ MNOCProof

Q DP problem:
The TRS P consists of the following rules:

APP(app(app(rec, x0), x1), app(s, app(s, app(s, y_2)))) → APP(app(app(rec, x0), x1), app(s, app(s, y_2)))
APP(app(app(rec, x0), x1), app(s, 0)) → APP(app(x0, app(s, 0)), x1)
APP(app(app(rec, x0), x1), app(s, app(s, x2))) → APP(app(x0, app(s, app(s, x2))), app(app(x0, app(s, x2)), app(app(app(rec, x0), x1), x2)))
APP(app(app(rec, x0), x1), app(s, app(s, y_2))) → APP(app(app(rec, x0), x1), app(s, y_2))
APP(app(app(rec, app(app(rec, y_0), y_1)), x1), app(s, x2)) → APP(app(app(rec, y_0), y_1), app(s, x2))
APP(app(app(rec, app(app(rec, y_0), y_1)), x1), app(s, 0)) → APP(app(app(rec, y_0), y_1), app(s, 0))
APP(app(app(rec, app(app(rec, y_0), y_1)), x1), app(s, app(s, 0))) → APP(app(app(rec, app(app(rec, y_0), y_1)), x1), app(s, 0))
APP(app(app(rec, x0), x1), app(s, app(s, 0))) → APP(app(app(rec, x0), x1), app(s, 0))
APP(app(app(rec, app(app(rec, y_0), y_1)), x1), app(s, app(s, y_2))) → APP(app(app(rec, y_0), y_1), app(s, app(s, y_2)))
APP(app(app(rec, app(app(rec, y_0), y_1)), x1), app(s, app(s, y_3))) → APP(app(app(rec, app(app(rec, y_0), y_1)), x1), app(s, y_3))
APP(app(app(rec, app(app(rec, y_0), y_1)), x1), app(s, app(s, app(s, y_3)))) → APP(app(app(rec, app(app(rec, y_0), y_1)), x1), app(s, app(s, y_3)))

The TRS R consists of the following rules:

app(app(app(rec, f), x), 0) → x
app(app(app(rec, f), x), app(s, y)) → app(app(f, app(s, y)), app(app(app(rec, f), x), y))

The set Q consists of the following terms:

app(app(app(rec, x0), x1), 0)
app(app(app(rec, x0), x1), app(s, x2))

We have to consider all minimal (P,Q,R)-chains.
We use the modular non-overlap check [17] to decrease Q to the empty set.

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ Narrowing

            ↳ QDP

              ↳ ForwardInstantiation

                ↳ QDP

                  ↳ ForwardInstantiation

                    ↳ QDP

                      ↳ MNOCProof

                        ↳ QDP

          ↳ MNOCProof

Q DP problem:
The TRS P consists of the following rules:

APP(app(app(rec, x0), x1), app(s, 0)) → APP(app(x0, app(s, 0)), x1)
APP(app(app(rec, x0), x1), app(s, app(s, app(s, y_2)))) → APP(app(app(rec, x0), x1), app(s, app(s, y_2)))
APP(app(app(rec, x0), x1), app(s, app(s, x2))) → APP(app(x0, app(s, app(s, x2))), app(app(x0, app(s, x2)), app(app(app(rec, x0), x1), x2)))
APP(app(app(rec, app(app(rec, y_0), y_1)), x1), app(s, x2)) → APP(app(app(rec, y_0), y_1), app(s, x2))
APP(app(app(rec, x0), x1), app(s, app(s, y_2))) → APP(app(app(rec, x0), x1), app(s, y_2))
APP(app(app(rec, app(app(rec, y_0), y_1)), x1), app(s, 0)) → APP(app(app(rec, y_0), y_1), app(s, 0))
APP(app(app(rec, app(app(rec, y_0), y_1)), x1), app(s, app(s, 0))) → APP(app(app(rec, app(app(rec, y_0), y_1)), x1), app(s, 0))
APP(app(app(rec, x0), x1), app(s, app(s, 0))) → APP(app(app(rec, x0), x1), app(s, 0))
APP(app(app(rec, app(app(rec, y_0), y_1)), x1), app(s, app(s, y_2))) → APP(app(app(rec, y_0), y_1), app(s, app(s, y_2)))
APP(app(app(rec, app(app(rec, y_0), y_1)), x1), app(s, app(s, y_3))) → APP(app(app(rec, app(app(rec, y_0), y_1)), x1), app(s, y_3))
APP(app(app(rec, app(app(rec, y_0), y_1)), x1), app(s, app(s, app(s, y_3)))) → APP(app(app(rec, app(app(rec, y_0), y_1)), x1), app(s, app(s, y_3)))

The TRS R consists of the following rules:

app(app(app(rec, f), x), 0) → x
app(app(app(rec, f), x), app(s, y)) → app(app(f, app(s, y)), app(app(app(rec, f), x), y))

Q is empty.
We have to consider all (P,Q,R)-chains.
We use the modular non-overlap check [17] to decrease Q to the empty set.

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ Narrowing

          ↳ MNOCProof

            ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

APP(app(app(rec, f), x), app(s, y)) → APP(f, app(s, y))
APP(app(app(rec, f), x), app(s, y)) → APP(app(app(rec, f), x), y)
APP(app(app(rec, f), x), app(s, y)) → APP(app(f, app(s, y)), app(app(app(rec, f), x), y))

The TRS R consists of the following rules:

app(app(app(rec, f), x), 0) → x
app(app(app(rec, f), x), app(s, y)) → app(app(f, app(s, y)), app(app(app(rec, f), x), y))

Q is empty.
We have to consider all (P,Q,R)-chains.